$\forall$$S$:RealizerScheme\{i:l\}(), $P$, $Q$:(ES$\rightarrow\mathbb{P}$).
\\[0ex]$S$ $\mid${-}${\it es}$.$P$(${\it es}$) $\Rightarrow$ ($\forall$${\it es}$:ES. $P$(${\it es}$) $\Rightarrow$ $Q$(${\it es}$)) $\Rightarrow$ $S$ $\mid${-}${\it es}$.$Q$(${\it es}$)